PRISM
=====
Version: 4.5
Date: Wed Apr 01 08:58:58 UTC 2020
Hostname: cb4ac6bf600d
Memory limits: cudd=1g, java(heap)=2g
Type: CTMC
Modules: D_def Y_def Z_def CC_def XX_def EE_def
Variables: D Y Z CC XX EE
Generator: stamina.InfCTMCModelGenerator
Type: CTMC
========================================================================
Approximation<1> : kappa = 1.0E-6
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 22 5168 states
5168 states
Reachable states exploration and model construction done in 1.938 secs.
Sorting reachable states list...
Time for model construction: 1.968 seconds.
Type: CTMC
States: 5168 (1 initial)
Transitions: 42949
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((EE>40&(!EE=-1))&(CC<20&(!CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 8.616 seconds.
Value in the initial state: 0.0
Time for model checking: 8.643 seconds.
Result: 0.0 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((EE>40|(EE=-1))&(CC<20|(CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 8.796 seconds.
Value in the initial state: 0.0830190021399403
Time for model checking: 8.803 seconds.
Result: 0.0830190021399403 (value in the initial state)
========================================================================
Approximation<2> : kappa = 9.999999999999999E-10
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 35566 37842 38691 39147 39597 39671 states
1 39671 states
Reachable states exploration and model construction done in 16.76 secs.
Sorting reachable states list...
Time for model construction: 16.836 seconds.
Type: CTMC
States: 39671 (1 initial)
Transitions: 361885
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((EE>40&(!EE=-1))&(CC<20&(!CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.287226595180127 x 2100.0 = 6903.1758498782665
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 136.264 seconds.
Value in the initial state: 0.05007058777924607
Time for model checking: 136.303 seconds.
Result: 0.05007058777924607 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((EE>40|(EE=-1))&(CC<20|(CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.287226595180127 x 2100.0 = 6903.1758498782665
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 136.303 seconds.
Value in the initial state: 0.055952025386081815
Time for model checking: 136.323 seconds.
Result: 0.055952025386081815 (value in the initial state)
========================================================================
Approximation<3> : kappa = 9.999999999999998E-13
========================================================================
---------------------------------------------------------------------
Building model...
Computing reachable states... 100360 117112 119221 119267 states
1 119267 states
Reachable states exploration and model construction done in 11.685 secs.
Sorting reachable states list...
Time for model construction: 11.985 seconds.
Type: CTMC
States: 119267 (1 initial)
Transitions: 1178621
---------------------------------------------------------------------
Verifying Lower Bound for change_state_min .....
---------------------------------------------------------------------
Model checking: "change_state_min": P=? [ F<=T ((EE>40&(!EE=-1))&(CC<20&(!CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 291.832 seconds.
Value in the initial state: 0.05427187832831769
Time for model checking: 291.855 seconds.
Result: 0.05427187832831769 (value in the initial state)
---------------------------------------------------------------------
Verifying Upper Bound for change_state_max .....
---------------------------------------------------------------------
Model checking: "change_state_max": P=? [ F<=T ((EE>40|(EE=-1))&(CC<20|(CC=-1))) ]
Property constants: T=2100
Starting backwards transient probability computation...
Uniformisation: q.t = 3.2872265951801265 x 2100.0 = 6903.175849878266
Fox-Glynn (1.25E-7): left = 6319, right = 7610
Backwards transient probability computation took 7611 iters and 290.554 seconds.
Value in the initial state: 0.054320821709538454
Time for model checking: 290.57 seconds.
Result: 0.054320821709538454 (value in the initial state)
========================================================================
Property: "change_state": P=? [ F<=T ((EE>40)&(CC<20)) ]
ProbMin: 0.05427187832831769 (value in the initial state)
ProbMax: 0.054320821709538454 (value in the initial state)
========================================================================